; Exercise 1.13: Prove that Fib(n) is the closest integer to
;
;  phi^n
; -------
; sqrt(5)
;
;             1 + sqrt(5)
; where phi = -----------.
;                  2
;
;                  1 - sqrt(5)
;  Hint: Let psi = ----------- . (1)
;                       2

; Use induction and the definition of the Fibonacci numbers to prove that

;           phi^n - psi^n
;  Fib(n) = ------------- . (2)
;              sqrt(5)
;

; Here's the definition of Fib(n):

;          /
;          | 0 if n = 0
; Fib(n) = < 1 if n = 1                         (3)
;          | Fib(n - 1) + Fib(n - 2) otherwise
;          \
;

; First, let us prove the formula for the base cases. What we have here is:

;            phi^0 - psi^0
;  Fib(0) =  ------------- = 0
;                sqrt(5)

;            phi^1 - psi^1   sqrt(5)
;  Fib(1) =  ------------- = ------- = 1
;              sqrt(5)       sqrt(5)

; So far, so good. We have the basis proved, now for the inductive step...

; Assuming that (2) is true for all integers up to n-1, we have to prove that
; (2) is a formula that gives the value of the n-th Fibonacci number.

; For that, let us use the expanded form of Fib(n-1) and Fib(n-2), which is
; true by our hypothesis.

; Fib(n-1) = phi^(n-1) - psi^(n-1)
;            ---------------------
;                 sqrt(5)

; Fib(n-2) = phi^(n-2) - psi^(n-2)
;            -----------------------
;                 sqrt(5)

; Now, applying the definition of the Fibonacci function, we have:

;                                  phi^(n-1) - psi^(n-1)   phi^(n-2) - psi^(n-2)
;  Fib(n) = Fib(n-1) + Fib(n-2) =  ----------------------- + ----------------------- =
;                                         sqrt(5)                   sqrt(5)
;
;       1
;  = ------- (phi^(n-1) + phi^(n-2) - (psi^(n-1) + psi^(n-2))) =
;    sqrt(5)
;
;        1      phi^n   phi^n     psi^n   psi^n
;  =  ------- [ ----- + ----- - ( ----- + ----- )] =
;     sqrt(5)    phi    phi^2       psi   psi^2
;
;        1            phi+1         psi+1
;  =  ------- ( phi^n ----- - psi^n ----- )
;     sqrt(5)         phi^2         psi^2

; As is noted on the book, phi^2 = phi + 1. Luckily, the same property holds
; for psi. So...

;        1                       phi^n - psi^n  *
;  =  ------- ( phi^n - psi^n) = -------------  = Fib(n).
;     sqrt(5)                      sqrt(5)

; * This last equality holds by assumption. Anyway, our proof is complete.

; By the way,

; phi^2 = phi + 1 = 2.6180339887498949
; psi^2 = psi + 1 = 0.3819660112501051



